package br.ufrgs.inf.inf05516

/**
 * ***************************************
 * Classes para expressões e tipos de L3
 * Não mexer!!!
 * ***************************************
 */
abstract class Tipo
case class TyInt() extends Tipo
case class TyBool() extends Tipo
case class TyUnit() extends Tipo
case class TyFun(t1: Tipo, t2: Tipo) extends Tipo
case class TyRef(t: Tipo) extends Tipo
case class TyReg(eltos: List[(String, Tipo)]) extends Tipo
case class TyTop() extends Tipo

abstract class Oper
case class Sum() extends Oper
case class Prod() extends Oper
case class Dif() extends Oper
case class Eq() extends Oper

abstract class Expr
case class N(n: Int) extends Expr
case class B(b: Boolean) extends Expr
case class BinOp(op: Oper, e1: Expr, e2: Expr) extends Expr
case class If(e1: Expr, e2: Expr, e3: Expr) extends Expr
case class Asg(e1: Expr, e2: Expr) extends Expr
case class Deref(e: Expr) extends Expr
case class Ref(e: Expr) extends Expr
case class Skip() extends Expr
case class Seq(e1: Expr, e2: Expr) extends Expr
case class W(e1: Expr, e2: Expr) extends Expr
case class Fun(x: String, t: Tipo, e: Expr) extends Expr
case class App(e1: Expr, e2: Expr) extends Expr
case class Id(x: String) extends Expr
case class Let(x: String, t: Tipo, e1: Expr, e2: Expr) extends Expr
case class Reg(eltos: List[(String, Expr)]) extends Expr
case class Proj(lab: String, e: Expr) extends Expr
/**
 * ***************************************
 * Classes para expressões e tipos de L3
 * Não mexer!!!
 * ***************************************
 */

class L3Interpreter {

  /**
   * The type-check method returns the type of the expression
   * Make sure gamma's List type match Gamma's declaration type (was out of scope)!
   */
  def typecheck(e: Expr, gamma: List[(String, Tipo)]): Option[Tipo] = e match {

    // Integer
    case N(_) => Some(TyInt())

    // Boolean
    case B(_) => Some(TyBool())

    // Binary Operation :Some(TyInt())
    case BinOp(op: Oper, e1: Expr, e2: Expr) => op match {
      // + :Some(TyInt())
      case Sum() => (typecheck(e1, gamma), typecheck(e2, gamma)) match {
        case (Some(TyInt()), Some(TyInt())) => Some(TyInt())
        case (_) => None
      }
      // * :Some(TyInt())
      case Prod() => (typecheck(e1, gamma), typecheck(e2, gamma)) match {
        case (Some(TyInt()), Some(TyInt())) => Some(TyInt())
        case (_) => None
      }
      // - :Some(TyInt())
      case Dif() => (typecheck(e1, gamma), typecheck(e2, gamma)) match {
        case (Some(TyInt()), Some(TyInt())) => Some(TyInt())
        case (_) => None
      }
      // = :Some(TyBool())
      case Eq() => (typecheck(e1, gamma), typecheck(e2, gamma)) match {
        case (Some(TyInt()), Some(TyInt())) => Some(TyBool())
        case (_) => None
      }
    }

    // If :Some(Type of e2 or e3)
    case If(e1, e2, e3) => (typecheck(e1, gamma), typecheck(e2, gamma), typecheck(e3, gamma)) match {
      case (_, _, None) => None
      case (_, None, _) => None
      case (Some(TyBool()), t2, t3) => join(t2.get, t3.get)
      case _ => None
    }

    // Attribution :Some(TyUnit())
    case Asg(e1, e2) => (typecheck(e1, gamma), typecheck(e2, gamma)) match {
      // TODO exigir t==t2 é muito restritivo, poderíamos flexibilizar o programa usando subtipagem. Dica do Álvaro
      case (Some(TyRef(t)), Some(t2)) => if (t == t2) { Some(TyUnit()) } else None
      case (_) => None
    }

    // Deref :Some(Tipo)
    case Deref(e) => (typecheck(e, gamma)) match {
      case Some(TyRef(t)) => Some(t)
      case (_) => None
    }

    // Ref :Some(TyRef(Tipo))
    case Ref(e: Expr) => (typecheck(e, gamma)) match {
      case Some(t) => Some(TyRef(t))
      case (_) => None
    }

    // Skip :Some(TyUnit())
    case Skip() => Some(TyUnit())

    // Sequence :Some(Type of e2)
    case Seq(e1, e2) => (typecheck(e1, gamma)) match {
      case (Some(TyUnit())) => typecheck(e2, gamma)
      case (_) => None
    }

    // While :Some(TyUnit())
    case W(e1, e2) => (typecheck(e1, gamma), typecheck(e2, gamma)) match {
      case (Some(TyBool()), Some(TyUnit())) => Some(TyUnit())
      case (_) => None
    }

    // Function :Some(TyFun())
    case Fun(s: String, t: Tipo, e) =>
      var gammaTmp = (s, t) :: gamma
      val t1: Option[Tipo] = typecheck(e, gammaTmp)
      if (t1 != None) {
        Some(TyFun(t, t1.get))
      } else None

    // Application :Some(Out type of e1)
    case App(e1, e2) => (typecheck(e1, gamma), typecheck(e2, gamma)) match {
      case (Some(TyFun(t11, t12)), Some(t2)) =>
        if (subtype(t2, t11)) {
          Some(t12)
        } else { None }
      case (_) => None
    }

    // Identifier :Some(Type of s)
    case Id(s) =>
      if (!gamma.isEmpty) {
        val v = s
        var found = false
        var gammaTmp: List[(String, Tipo)] = gamma
        var tmp: (String, Tipo) = gammaTmp.head
        while (!gammaTmp.isEmpty && !found) {
          tmp = gammaTmp.head
          if (tmp._1 == v) {
            found = true
          }
          gammaTmp = gammaTmp.tail
        }
        if (found) {
          Some(tmp._2)
        } else None
      } else None

    // Let :Some(Out type of e2)
    case Let(s: String, t: Tipo, e1, e2) =>
      typecheck((App(Fun(s, t, e2), e1)), gamma)

    // Register :Some(List(String, Tipo))
    case Reg(eltos) =>
      var list: List[(String, Tipo)] = List()
      for (el <- eltos) {
        list = list ::: List((el._1, typecheck(el._2, gamma).get))
      }; Some(TyReg(list))

    // Projection
    case Proj(s: String, e: Expr) => (s, typecheck(e, gamma)) match {
      case (lab, Some(TyReg(eltos))) =>
        // typecheck(e, gamma) gave us a registry with labels and its types 
        for (el <- eltos) {
          // check if we found the label in the registry
          if (el._1.equals(lab)) {
            // return its type
            return Some(el._2)
          }
        }; None
      case (_) => None
    }

    case t @ (_) => println("Tipagem ainda não implementada para o tipo "+t); None

  }

  /**
   * Checks if a type s is sub-type of a type t
   */
  def subtype(s: Tipo, t: Tipo): Boolean = (s, t) match {
    // TODO join e meet contemplam Ref, mas subtype não! Foi perguntado pelo Álavro
    // one function is sub-type of another
    case (TyFun(s1, s2), TyFun(t1, t2)) => subtype(t1, s1) && subtype(s2, t2)
    // one registry is sub-type of another
    case (s @ TyReg(eltosS), t @ TyReg(eltosT)) =>
      // check if all elements of the father are in the son
      for (tEl <- t.eltos) {
        if (!s.eltos.contains(tEl)) {
          // before we return with false:
          // if the son does not contain the exact element,
          // we must check if it contains one with the same LABEL and with a SUBTYPE 
          var found = false
          for (sEl <- s.eltos) {
            if (sEl._1.equals(tEl._1)) {
              found = true
              if (!subtype(sEl._2, tEl._2)) {
                return false; // ok, then fail
              }
            }
          }
          // did we found it?
          if (!found) {
            return false; // ok, then fail
          }
        }
      }; true
    // s is sub-type of top
    case (_, TyTop()) => true
    // s is the same type as t
    case (s, t) => if (s == t) true else false
  }

  /**
   * Checks for the higher common father of both types.
   *
   * It never returns None because TyTop() is always
   * a valid option, but we still return Option[Tipo]
   * for consistency with meet(s:Tipo,t:Tipo):Option[Tipo].
   * That guy may return None.
   */
  def join(s: Tipo, t: Tipo): Option[Tipo] = (s, t) match {
    // join of function
    case (TyFun(s1, s2), TyFun(t1, t2)) =>
      (meet(s1, t1), join(s2, t2)) match {
        case (None, j2) => Some(TyTop()) // Álvaro confirmed
        case (m1, j2) => Some(TyFun(m1.get, j2.get))
      }
    // join of References
    case (TyRef(s1), TyRef(t1)) =>
      if (subtype(s1, t1) && subtype(t1, s1)) {
        Some(TyRef(t1))
      } else {
        None
      }
    // join of registers
    case (TyReg(eltosS), TyReg(eltosT)) =>
      var list: List[(String, Tipo)] = List(); // result list is
      for (sEl <- eltosS) {
        for (tEl <- eltosT) {
          if (sEl._1.equals(tEl._1)) { // intersection of labels
            join(sEl._2, tEl._2) match { // plus join of associated types
              case Some(t) => list = list ::: List((sEl._1, t))
              case _ => list = list ::: List((sEl._1, TyTop()))
            }
          }
        }
      }
      Some(TyReg(list))
    // else
    case (s, t) => if (s == t) Some(s) else Some(TyTop())
  }

  /**
   * Checks for the first sub-type that extends
   * both types
   */
  def meet(s: Tipo, t: Tipo): Option[Tipo] = (s, t) match {
    // TyReg
    case (TyReg(eltosS), TyReg(eltosT)) =>
      var list: List[(String, Tipo)] = List();
      for (sEl <- eltosS) {
        var found = false
        for (tEl <- eltosT) {
          if (sEl._1.equals(tEl._1)) { //labels in S and T
            found = true;
            val meettype = meet(sEl._2, tEl._2)
            if (meettype != None) {
              list = list ::: List((sEl._1, meettype.get))
            } // TODO what if meet is None?
          }
        }
        // if we didn't found
        if (!found) { // labels in S that are not in T
          list = list ::: List(sEl)
        }
      }
      // labels in T that are not in S
      for (tEl <- eltosT) {
        var found = false
        for (sEl <- eltosS) {
          if (sEl._1.equals(tEl._1)) {
            found = true
          }
        }
        if (!found) {
          list = list ::: List(tEl)
        }
      }
      Some(TyReg(list))
    // join of References
    case (TyRef(s1), TyRef(t1)) =>
      if (subtype(s1, t1) && subtype(t1, s1)) {
        Some(TyRef(t1))
      } else {
        None
      }
    // TyFun
    case (TyFun(s1, s2), TyFun(t1, t2)) => (join(s1, t1), meet(s2, t2)) match {
      case (_, None) => None // TODO Is it right???
      case (j, m) => Some(TyFun(j.get, m.get))
    }
    // TyTop's
    case (TyTop(), t) => Some(t)
    case (s, TyTop()) => Some(s)
    // Normal types
    case (s, t) => if (s == t) {
      s match {
        case TyInt() => Some(TyInt())
        case TyBool() => Some(TyBool())
        case (_) => None
      }
    } else {
      None
    }
  }
}

// L3 Object
object L3 {

  // type definition for inside our program (helps to avoid mistakes)
  type Rotulo = String
  type Gamma = List[(Rotulo, Tipo)]

  // Main method
  def main(args: Array[String]) {

    // Gamma: (label -> type) mapping
    val gamma: Gamma = List()

    /**
     * Define tests for our typechecker
     */
    def tests: Unit = {
      println("/******************************** ")
      println(" ************ TESTES ************ ")
      println(" ********************************/")
      val interpretador = new L3Interpreter()

      // Tests from "Exercicios de Semantica Operacional e Sist de Tipos"
      // pag 10 ex 1.30
      // (fn x:{A:Bool} => if #A x then 2 else 3) {A=true,B=10}
      val exercise_1_30: Expr =
        App(
          Fun(
            "x",
            TyReg(List(("A", TyBool()))),
            If(
              Proj(
                "A",
                Id("x")),
              N(2),
              N(3))),
          Reg(List(("A", B(true)), ("B", N(10)))))
      interpretador.typecheck(exercise_1_30, gamma) match {
        case Some(TyInt()) => println("ok: exercise_1_30")
        case t @ _ => println("FAIL: exercise_1_30 should be TyInt(), found "+t)
      }

      // pag 4 ex 1.7
      // let x: int->int = fn y: int => y + 10 in x 10 end should be TyInt()
      val exercise_1_7: Expr =
        Let("x", TyFun(TyInt(), TyInt()), Fun("y", TyInt(), BinOp(Sum(), Id("y"), N(10))), App(Id("x"), N(10)))
      interpretador.typecheck(exercise_1_7, gamma) match {
        case Some(TyInt()) => println("ok: exercise_1_7")
        case t @ _ => println("FAIL: exercise_1_7 should be TyInt(), was "+t)
      }

      // pag 2 ex 1.3:
      // (l2:=0); while !l1 >= 0 do (l2:=(!l2+!l1);(l1:=(!l1+ -1))) should be TyUnit()
      // with gamma={l1:int ref, l2:int ref, l3: int ref}
      var gamma_exercise_1_3 = List(("l1", TyRef(TyInt())), ("l2", TyRef(TyInt())), ("l3", TyRef(TyInt())))
      val exercise_1_3: Expr =
        Seq(
          Asg(
            Id("l2"),
            N(0)),
          W(
            BinOp(
              Eq(),
              Deref(Id("l1")),
              N(0)),
            Seq(
              Asg(
                Id("l2"),
                BinOp(
                  Sum(),
                  Deref(Id("l2")),
                  Deref(Id("l1")))),
              Asg(
                Id("l1"),
                BinOp(
                  Sum(),
                  Deref(Id("l1")),
                  N(-1))))));
      interpretador.typecheck(exercise_1_3, gamma_exercise_1_3) match {
        case Some(TyUnit()) => println("ok: exercise_1_3")
        case t @ _ => println("FAIL:exercise_1_3 should be TyUnit(), found "+t)
      }

      // Tests from Alvaro's email
      var alvaro_4: Expr = Let("f", TyFun(TyReg(List(("a", TyInt()), ("b", TyBool()))), TyReg(List(("a", TyInt()), ("b", TyBool())))),
        Fun("x", TyReg(List(("a", TyInt()), ("b", TyBool()))), Id("x")),
        Let("rab", TyReg(List(("a", TyInt()))), Reg(List(("a", N(0)), ("b", B(true)))), Proj("b", App(Id("f"), Id("rab")))))
      interpretador.typecheck(alvaro_4, gamma) match {
        case Some(t) =>
          println("FAIL alvaro_4: expressao mal tipada foi avaliada para "+t)
        case _ =>
          println("ok: alvaro_4")
      }
      var alvaro_3: Expr = App(Fun("r", TyRef(TyReg(List(("x", TyInt()), ("y", TyInt())))), Proj("y", Deref(Id("r")))), Ref(Reg(List(("x", N(0))))))
      interpretador.typecheck(alvaro_3, gamma) match {
        case Some(t) =>
          println("FAIL: alvaro_3 expressao mal tipada foi avaliada para "+t)
        case _ =>
          println("ok: alvaro_3")
      }
      var alvaro_2: Expr = App(Fun("r", TyRef(TyReg(List(("x", TyInt()), ("y", TyInt())))), Seq(Asg(Id("r"), Reg(List(("x", N(1))))), Proj("y", Deref(Id("r"))))), Ref(Reg(List(("x", N(0)), ("y", N(1))))))
      interpretador.typecheck(alvaro_2, gamma) match {
        case Some(t) =>
          println("FAIL: alvaro_2 expressao mal tipada foi avaliada para "+t)
        case _ =>
          println("ok: alvaro_2")
      }
      var alvaro_1: Expr = App(Fun("r", TyReg(List(("x", TyTop()))), Proj("x", Id("r"))), Reg(List(("x", N(0)), ("y", N(1)))))
      interpretador.typecheck(alvaro_1, gamma) match {
        case Some(t) =>
          if (t == TyTop())
            println("ok: alvaro_1")
          else
            println("FAIL: alvaro_1 expressao tipo TyTop() incorretamente tipada para "+t)
        case _ =>
          println("FAIL: alvaro_1 expressao não foi tipada, era TyTop()")
      }

      // meet() : Some(Tipo)
      if (interpretador.meet(TyTop(), TyBool()) == Some(TyBool())) println("ok: meet #2") else println("FAIL: meet #2")
      if (interpretador.meet(TyInt(), TyTop()) == Some(TyInt())) println("ok: meet #1") else println("FAIL: meet #1")

      // join() : Some(Tipo)
      // TODO tests for join using functions
      // val f1 = TyFun(TyReg(List(("x", TyInt()))), TyBool())
      // val f2 = TyFun(TyReg(List(("x", TyInt()), ("y", TyInt()))), TyBool())
      // println(interpretador.join(f1, f2))
      if (interpretador.join( // join to an empty list
        TyReg(List(("x", TyInt()))),
        TyReg(List(("y", TyBool())))).get ==
        TyReg(List())) println("ok: join #5") else println("FAIL: join #5")
      if (interpretador.join( // join for the common element of the list, using TyTop() as type
        TyReg(List(("x", TyInt()))),
        TyReg(List(("x", TyBool()), ("y", TyBool())))).get ==
        TyReg(List(("x", TyTop())))) println("ok: join #4") else println("FAIL: join #4")
      if (interpretador.join( // join for the common element of the list
        TyReg(List(("x", TyInt()))),
        TyReg(List(("x", TyInt()), ("y", TyBool())))).get ==
        TyReg(List(("x", TyInt())))) println("ok: join #3") else println("FAIL: join #3")
      if (interpretador.join(TyInt(), TyInt()).get == TyInt()) println("ok: join #2") else println("FAIL: join #2")
      if (interpretador.join(TyInt(), TyBool()).get == TyTop()) println("ok: join #1") else println("FAIL: join #1")

      // subtype() :TyBool()
      val funS1S2_subtype6 = TyFun(TyReg(List(("x", TyInt()))), TyReg(List(("k", TyInt()), ("w", TyBool()))))
      val funT1T2_subtype6 = TyFun(TyReg(List(("x", TyInt()), ("y", TyBool()))), TyReg(List(("k", TyInt()))))
      if (interpretador.subtype(funS1S2_subtype6, funT1T2_subtype6)) {
        println("ok: subtype() #6")
      } else {
        println("FAIL: subtype() #6 funtion s1->s2 is subtype of function t1->t2")
      }
      if (interpretador.subtype( // s doesn`t have all elements of the father t -> false
        TyReg(List(("x", TyInt()))),
        TyReg(List(("x", TyInt()), ("y", TyBool()))))) println("FAIL: subtype() #5") else println("ok: subtype() #5");
      if (interpretador.subtype( // s has all elements of the father t, and they are subtype -> true
        TyReg(List(("x", TyInt()), ("y", TyBool()))),
        TyReg(List(("x", TyTop()))))) println("ok: subtype() #4") else println("FAIL: subtype() #4");
      if (interpretador.subtype( // s has all elements of the father t -> true
        TyReg(List(("x", TyInt()), ("y", TyBool()))),
        TyReg(List(("x", TyInt()))))) println("ok: subtype() #3") else println("FAIL: subtype() #3");
      if (interpretador.subtype( // son of TyTop() -> true
        TyInt(),
        TyTop())) println("ok: subtype() #2") else println("FAIL: subtype() #2");
      if (interpretador.subtype( // different types -> false
        TyInt(),
        TyBool())) println("FAIL: subtype() #1") else println("ok: subtype() #1");
      if (interpretador.subtype( // same types -> true
        TyInt(),
        TyInt())) println("ok: subtype() #0") else println("FAIL: subtype() #0");

      // Proj: example #x {x=0, y=false, z=true} should return TyInt()
      val proj_2: Expr = Proj("y", Reg(List(("x", N(0)), ("y", B(false)), ("z", B(true)))))
      interpretador.typecheck(proj_2, gamma) match {
        case Some(TyBool()) => println("ok: proj_2")
        case t @ _ => println("FAIL: proj_2, tipo retornado deveria ser TyBool(), encontrado "+t)
      }
      val proj_1: Expr = Proj("x", Reg(List(("x", N(0)), ("y", B(false)), ("z", B(true)))))
      interpretador.typecheck(proj_1, gamma) match {
        case Some(TyInt()) => println("ok: proj_1")
        case t @ _ => println("FAIL: proj_1, tipo retornado deveria ser TyInt(), encontrado "+t)
      }

      // If: Some(Tipo)
      val if_4: Expr = If(BinOp(Eq(), N(1), N(2)),
        Reg(List(("x", N(5)))),
        Reg(List(("x", N(5)), ("y", B(true))))) // e1's type is sub-type of e2's type
      interpretador.typecheck(if_4, gamma) match {
        case Some(TyReg(eltos)) => if (eltos == List(("x", TyInt()))) println("ok: if_4 ") else println("FAIL: if_4"+eltos) //<- correct
        case None => println("FAIL: if_4")
      }
      val if_3: Expr = If(BinOp(Eq(), N(1), N(2)), Fun("x", TyInt(), N(5)), Fun("y", TyInt(), N(3))) // e1 and e2 have complex types
      interpretador.typecheck(if_3, gamma) match {
        case Some(tipo) => println("ok: if_3") //<- correct
        case None => println("FAIL: if_3")
      }
      val if_2: Expr = If(BinOp(Eq(), N(1), N(2)), B(true), N(5)) // e1 and e2 have different types
      interpretador.typecheck(if_2, gamma) match {
        case Some(tipo) => println("ok: if_2") //<- correct
        case None => println("FAIL: if_2")
      }
      val if_1: Expr = If(BinOp(Eq(), N(1), N(2)), N(4), N(5))
      interpretador.typecheck(if_1, gamma) match {
        case Some(tipo) => if (tipo == TyInt()) println("ok: if_1") else println("FAIL: if_1")
        case None => println("FAIL: if_1")
      }

      // = :TyBool()
      val binOpEq_2: Expr = BinOp(Eq(), BinOp(Dif(), N(1), N(2)), BinOp(Sum(), N(3), B(true)))
      interpretador.typecheck(binOpEq_2, gamma) match {
        case Some(tipo) => println("FAIL: binOpEq_2")
        case None => println("ok: binOpEq_2") // <- correct
      }
      val binOpEq_1: Expr = BinOp(Eq(), BinOp(Dif(), N(1), N(2)), BinOp(Sum(), N(3), N(4)))
      interpretador.typecheck(binOpEq_1, gamma) match {
        case Some(TyBool()) => println("ok: binOpEq_1") // <- correct: TyBool()
        case None => println("FAIL: binOpEq_1")
      }

      // - :TyInt()
      val binOpDif_3: Expr = BinOp(Dif(), BinOp(Sum(), N(1), N(2)), BinOp(Sum(), N(3), N(4)))
      interpretador.typecheck(binOpDif_3, gamma) match {
        case Some(TyInt()) => println("ok: binOpDif_3") // <- correct TyInt()
        case None => println("FAIL: binOpDif_3")
      }
      val binOpDif_2: Expr = BinOp(Dif(), BinOp(Dif(), N(1), N(2)), BinOp(Dif(), N(3), B(true)))
      interpretador.typecheck(binOpDif_2, gamma) match {
        case Some(tipo) => println("FAIL: binOpDif_2")
        case None => println("ok: binOpDif_2") // <- correct
      }
      val binOpDif_1: Expr = BinOp(Dif(), BinOp(Dif(), N(1), N(2)), BinOp(Dif(), N(3), N(4)))
      interpretador.typecheck(binOpDif_1, gamma) match {
        case Some(TyInt()) => println("ok: binOpDif_1") // <- correct: TyInt()
        case None => println("FAIL: binOpDif_1")
      }

      // * :TyInt()
      val binOpProd_2: Expr = BinOp(Prod(), BinOp(Prod(), N(1), N(2)), BinOp(Prod(), N(3), B(true)))
      interpretador.typecheck(binOpProd_2, gamma) match {
        case Some(tipo) => println("FAIL: binOpProd_2")
        case None => println("ok: binOpProd_2") // <- correct
      }
      val binOpProd_1: Expr = BinOp(Prod(), BinOp(Prod(), N(1), N(2)), BinOp(Prod(), N(3), N(4)))
      interpretador.typecheck(binOpProd_1, gamma) match {
        case Some(TyInt()) => println("ok: binOpProd_1") // <- correct: TyInt()
        case None => println("FAIL: binOpProd_1")
      }

      // + :TyInt()
      val binOpSum_2: Expr = BinOp(Sum(), BinOp(Sum(), N(1), N(2)), BinOp(Sum(), N(3), B(true)))
      interpretador.typecheck(binOpSum_2, gamma) match {
        case Some(tipo) => println("FAIL: binOpSum_2")
        case None => println("ok: binOpSum_2") // <- correct
      }
      val binOpSum_1: Expr = BinOp(Sum(), BinOp(Sum(), N(1), N(2)), BinOp(Sum(), N(3), N(4)))
      interpretador.typecheck(binOpSum_1, gamma) match {
        case Some(TyInt()) => println("ok: binOpSum_1") // <- correct: TyInt()
        case None => println("FAIL: binOpSum_1")
      }

      // Let :Some(Out type of e2)
      val Let_5: Expr = Let("y", TyInt(), N(0), BinOp(Prod(), Id("y"), N(8)))
      interpretador.typecheck(Let_5, gamma) match {
        case Some(TyInt()) => println("ok: Let_5") // <- correct: TyInt()
        case None => println("FAIL: Let_5")
      }
      val Let_4: Expr = Let("r", TyBool(), B(true), BinOp(Prod(), Id("r"), N(8)))
      interpretador.typecheck(Let_4, gamma) match {
        case Some(tipo) => println("FAIL: Let_4")
        case None => println("ok: Let_4") // <- correct
      }
      val Let_3: Expr = Let("r", TyBool(), B(true), If(Id("r"), B(true), N(8)))
      interpretador.typecheck(Let_3, gamma) match {
        case Some(TyTop()) => println("ok: Let_3") // <- correct TyTop()
        case None => println("FAIL: Let_3")
      }
      val Let_2: Expr = Let("j", TyBool(), B(true), If(Id("j"), N(0), N(8)))
      interpretador.typecheck(Let_2, gamma) match {
        case Some(TyInt()) => println("ok: Let_2") // <- correct: TyInt()
        case None => println("FAIL: Let_2")
      }
      val Let_1: Expr = Let("y", TyInt(), N(0), BinOp(Prod(), Id("x"), N(8)))
      interpretador.typecheck(Let_1, gamma) match {
        case Some(tipo) => println("FAIL: Let_1")
        case None => println("ok: Let_1") // <- correct
      }

      // While :Some(TyUnit())
      val W_4: Expr = W(If(BinOp(Eq(), (BinOp(Sum(), N(1), N(8))), N(8)), B(true), B(true)), W((BinOp(Eq(), N(1), N(8))), Seq(Skip(), Skip())))
      interpretador.typecheck(W_4, gamma) match {
        case Some(TyUnit()) => println("ok: W_4") // <- correct: TyUnit()
        case None => println("FAIL: W_4")
      }
      val W_3: Expr = W(If(BinOp(Eq(), N(1), N(8)), N(1), N(8)), Seq(Skip(), Skip()))
      interpretador.typecheck(W_3, gamma) match {
        case Some(tipo) => println("FAIL: W_3")
        case None => println("ok: W_3") // <- correct: TyUnit()
      }
      val W_2: Expr = W((BinOp(Sum(), N(1), N(8))), Seq(Skip(), Skip()))
      interpretador.typecheck(W_2, gamma) match {
        case Some(tipo) => println("FAIL: W_2")
        case None => println("ok: W_2") // <- correct
      }
      val W_1: Expr = W((BinOp(Eq(), N(1), N(8))), Seq(Skip(), Skip()))
      interpretador.typecheck(W_1, gamma) match {
        case Some(TyUnit()) => println("ok: W_1") // <- correct: TyUnit()
        case None => println("FAIL: W_1")
      }

      // Sequence :Some(Type of e2)
      val Seq_4: Expr = Seq((Seq(Skip(), Skip())), (Seq((Seq(Skip(), Skip())), Skip())))
      interpretador.typecheck(Seq_4, gamma) match {
        case Some(TyUnit()) => println("ok: Seq_4") // <- correct: TyUnit()
        case None => println("FAIL: Seq_4")
      }
      val Seq_3: Expr = Seq(BinOp(Sum(), N(1), N(8)), Skip())
      interpretador.typecheck(Seq_3, gamma) match {
        case Some(tipo) => println("FAIL: Seq_3")
        case None => println("ok: Seq_3") // <- correct
      }
      val Seq_2: Expr = Seq((W((BinOp(Eq(), N(1), N(8))), Seq(Skip(), Skip()))), Skip())
      interpretador.typecheck(Seq_2, gamma) match {
        case Some(TyUnit()) => println("ok: Seq_2") // <- correct: TyUnit()
        case None => println("FAIL: Seq_2")
      }
      val Seq_1: Expr = Seq(Skip(), Skip())
      interpretador.typecheck(Seq_1, gamma) match {
        case Some(TyUnit()) => println("ok: Seq_1") // <- correct: TyUnit()
        case None => println("FAIL: Seq_1")
      }

      // Function :Some(TyFun())
      val Fun_4: Expr = Fun("x", TyInt(), (Seq((Seq(Skip(), Skip())), Skip())))
      interpretador.typecheck(Fun_4, gamma) match {
        case Some(TyFun(TyInt(), TyUnit())) => println("ok: Fun_4") // <- correct: TyFun(TyInt(),TyUnit())
        case None => println("FAIL: Fun_4")
      }
      val Fun_3: Expr = Fun("x", TyInt(), BinOp(Sum(), N(1), Id("y")))
      interpretador.typecheck(Fun_3, gamma) match {
        case Some(tipo) => println("FAIL: Fun_3")
        case None => println("ok: Fun_3") // <- correct
      }
      val Fun_2: Expr = Fun("x", TyInt(), Fun("x", TyInt(), BinOp(Sum(), N(1), Id("x"))))
      interpretador.typecheck(Fun_2, gamma) match {
        case Some(TyFun(TyInt(), TyFun(TyInt(), TyInt()))) => println("ok: Fun_2") // <- correct: TyFun(TyInt(),TyFun(TyInt(),TyInt()))
        case None => println("FAIL: Fun_2")
      }
      val Fun_1: Expr = Fun("x", TyInt(), BinOp(Sum(), N(1), Id("x")))
      interpretador.typecheck(Fun_1, gamma) match {
        case Some(TyFun(TyInt(), TyInt())) => println("ok: Fun_1") // <- correct: TyFun(TyInt(),TyInt())
        case None => println("FAIL: Fun_1")
      }

      // Application :Some(Out type of e1)
      val App_4: Expr = App((Fun("x", TyBool(), W(Id("x"), If(Id("x"), N(2), N(3))))), B(false))
      interpretador.typecheck(App_4, gamma) match {
        case Some(tipo) => println("FAIL: App_4")
        case None => println("ok: App_4") // <- correct
      }
      val App_3: Expr = App((Fun("x", TyUnit(), Seq(Id("x"), Skip()))), Skip())
      interpretador.typecheck(App_3, gamma) match {
        case Some(TyUnit()) => println("ok: App_3") // <- correct: TyUnit()
        case None => println("FAIL: App_3")
      }
      val App_2: Expr = App((Fun("x", TyInt(), (Fun("x", TyInt(), BinOp(Sum(), N(1), Id("x")))))), BinOp(Sum(), N(1), N(8)))
      interpretador.typecheck(App_2, gamma) match {
        case Some(TyFun(TyInt(), TyInt())) => println("ok: App_2") // <- correct: TyFun(TyInt(),TyInt())
        case None => println("FAIL: App_2")
      }
      val App_1: Expr = App((Fun("x", TyInt(), BinOp(Sum(), N(1), Id("x")))), BinOp(Sum(), N(1), N(8)))
      interpretador.typecheck(App_1, gamma) match {
        case Some(TyInt()) => println("ok: App_1") // <- correct: TyInt()
        case None => println("FAIL: App_1")
      }
    }
    // do the damn tests!
    tests;
  }
}